$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$$x$:$T$, $L$:$T$ List. sorted($L$) $\Rightarrow$ sorted(s{-}insert($x$;$L$)))